PRISM
=====
Version: 4.5.dev
Date: Sat Apr 03 04:30:17 CEST 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 philosophers-mdp.50.prism philosophers-mdp.50.props --property eat
Parsing model file "philosophers-mdp.50.prism"...
Type: MDP
Modules: phil1 phil2 phil3 phil4 phil5 phil6 phil7 phil8 phil9 phil10 phil11 phil12 phil13 phil14 phil15 phil16 phil17 phil18 phil19 phil20 phil21 phil22 phil23 phil24 phil25 phil26 phil27 phil28 phil29 phil30 phil31 phil32 phil33 phil34 phil35 phil36 phil37 phil38 phil39 phil40 phil41 phil42 phil43 phil44 phil45 phil46 phil47 phil48 phil49 phil50
Variables: p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39 p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50
Parsing properties file "philosophers-mdp.50.props"...
1 property:
(1) "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9))|((p31>=8)&(p31<=9))|((p32>=8)&(p32<=9))|((p33>=8)&(p33<=9))|((p34>=8)&(p34<=9))|((p35>=8)&(p35<=9))|((p36>=8)&(p36<=9))|((p37>=8)&(p37<=9))|((p38>=8)&(p38<=9))|((p39>=8)&(p39<=9))|((p40>=8)&(p40<=9))|((p41>=8)&(p41<=9))|((p42>=8)&(p42<=9))|((p43>=8)&(p43<=9))|((p44>=8)&(p44<=9))|((p45>=8)&(p45<=9))|((p46>=8)&(p46<=9))|((p47>=8)&(p47<=9))|((p48>=8)&(p48<=9))|((p49>=8)&(p49<=9))|((p50>=8)&(p50<=9)) ]
---------------------------------------------------------------------
Model checking: "eat": Pmax=? [ F ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9))|((p31>=8)&(p31<=9))|((p32>=8)&(p32<=9))|((p33>=8)&(p33<=9))|((p34>=8)&(p34<=9))|((p35>=8)&(p35<=9))|((p36>=8)&(p36<=9))|((p37>=8)&(p37<=9))|((p38>=8)&(p38<=9))|((p39>=8)&(p39<=9))|((p40>=8)&(p40<=9))|((p41>=8)&(p41<=9))|((p42>=8)&(p42<=9))|((p43>=8)&(p43<=9))|((p44>=8)&(p44<=9))|((p45>=8)&(p45<=9))|((p46>=8)&(p46<=9))|((p47>=8)&(p47<=9))|((p48>=8)&(p48<=9))|((p49>=8)&(p49<=9))|((p50>=8)&(p50<=9)) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 300 iterations in 478.15 seconds (average 1.593840, setup 0.00)
Time for model construction: 483.235 seconds.
Type: MDP
States: 4.876310850152259E49 (1 initial)
Transitions: 3.14160231535271E51
Choices: 2.8410165499519588E51
Transition matrix: 362750 nodes (3 terminal), 3.14160231535271E51 minterms, vars: 200r/200c/50nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 6 iterations in 2.56 seconds (average 0.427333, setup 0.00)
Prob1E: 7 iterations in 1.09 seconds (average 0.155714, setup 0.00)
yes = 4.876310850152259E49, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 3.794 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 487.844 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.